﻿/*****************************************************
 * File:            GraphDS.cs
 * Description:     Finding Distinguishing Set for a graph (Mealy machine or DFA)
 * By:              Ali Khalili (khalili DOT ir AT gmail DOT com)
 * Project:         Automata Learning
 * Requirements:    
 * Change log:
 *          -5 May 2013:  initial development
 * To Do:
 *          -[Merge this with W and Wp Method!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
 * License:
 *****************************************************/
using System;
using System.Collections.Generic;
using SMLib.Automata.Base;
using SMLib.Automata.DFA;
using SMLib.Automata.MM;
using SMLib.Base;

//using EnGine.Core;
//using AIDE.Base;
//
//using AIDE.Automata.DFA;
namespace MBT.GraphAlgorithms
{
	/// <summary>
	/// Graph Distinguishing Set Finder
	/// </summary>
	public class GraphDistingWords<STATETYPE, TRANSITIONTYPE>
	{
		IDiGraph<STATETYPE, TRANSITIONTYPE> myGraph;

		/// <summary>
		/// Constructor
		/// </summary>
		/// <param name="myGraph">the graph</param>
		public GraphDistingWords (IDiGraph<STATETYPE, TRANSITIONTYPE> myGraph)
		{
			this.myGraph = myGraph;
		}

		/// <summary>
		/// Create a new two dimentional array ([size][size])
		/// </summary>
		/// <typeparam name="T">of type T</typeparam>
		/// <param name="arr"></param>
		/// <param name="size">size of array</param>
		/// <returns></returns>
		T[][] NewTwoDimArray<T> (int size, int size2)
		{
			T[][] arr;
			arr = new T[size][];
			for (int i = 0; i < size; i++)
				arr [i] = new T[size2];
			return arr;
		}

		/// <summary>
		/// it is used in ComputeDistingiushingWords
		/// </summary>
		/// <param name="arr"></param>
		/// <param name="groups"></param>
		/// <param name="rowCount"></param>
		/// <param name="index1"></param>
		/// <param name="index2"></param>
		/// <returns></returns>
		int SameRow (int[][] arr, int[] groups, int rowCount, int index1, int index2)
		{
			for (int i = 0; i < rowCount; i++) {
				if (groups [arr [index1] [i]] == groups [arr [index2] [i]])
					continue;
				return i;
			}
			return -1;
		}

		int SameRow (int[][] stateTransitionOutputTable, int[][] stateTransitionTable, int[] partition, int numberOfTransitions, int indexOfS1, int indexOfS2)
		{
			/*Console.WriteLine ("{"+indexOfS1 + "-" + indexOfS2);
			for (int y=0; y<partition.Length; y++)
				Console.Write (partition [y] + " ");
			Console.WriteLine ("}");
			*/
			for (int i = 0; i < numberOfTransitions; i++) {
				//* if the destination does't exist
				if (stateTransitionTable [indexOfS1] [i] == -1 && stateTransitionTable [indexOfS2] [i] == -1)
					continue;

				if (stateTransitionTable [indexOfS1] [i] == -1 || stateTransitionTable [indexOfS2] [i] == -1)
					return i;

				//* if they result to the same output and to states in the same partition!
				if (partition [stateTransitionTable [indexOfS1] [i]] == partition [stateTransitionTable [indexOfS2] [i]]
				    && 
				    stateTransitionOutputTable [indexOfS1] [i] == stateTransitionOutputTable [indexOfS2] [i])
					continue;
				return i;
			}
			return -1;
		}

		/// <summary>
		/// Clone an array of integers
		/// </summary>
		/// <param name="arr"></param>
		/// <returns></returns>
		int[] CloneArray (int[] arr)
		{
			int[] c = new int[arr.Length];
			for (int i = 0; i < c.Length; i++)
				c [i] = arr [i];
			return c;
		}

		/// <summary>
		/// Computing the set of distinguihinhg words by construcing the k-equivalence partitions of M
		/// <para>
		/// Characterization set for machine M, denoted as W, is a finite 
		/// set of input sequences that distinguish the behavior of any 
		/// pair of states in M. 
		/// </para>
		/// </summary>
		/// <param name="computeAll">also store distinguishing words for each pair of </param>
		public List<Word> ComputeCharachterizationSet (bool computeAll = false)
		{
			////* if the set was given as the construction parameters (for example, 
			////* when using automata learning, we have this set), don't compute it again
			//if (DistinguishingWords != null && !computeAll)
			//    return null;

			List<Word> DistinguishingWords4Pairs = null;
			if (computeAll)
				DistinguishingWords4Pairs = new List<Word> ();

			List<Word> DistinguishingWords = new List<Word> ();

			int[] partitionTable = new int[this.myGraph.Size];

			Alphabet inputAlphabet = null;
			if (myGraph is MealyMachine) {
				inputAlphabet = (myGraph as MealyMachine).InputAlphabet;
			} else if (myGraph is DFA) {
				inputAlphabet = (myGraph as DFA).InputAlphabet;
			} else
				throw new Exception ("W-Method is working only with DFAs and Mealy machines!");

			List<int> groupHeaders = new List<int> ();
			List<List<int>> groups = new List<List<int>> ();

			//* state 0 is in group 0
			groupHeaders.Add (0);
			groups.Add (new List<int> ());
			groups [0].Add (0);

//			#region Compute k-equivalence partitions
//			#region Initialize
//
//			//* initialize groups
//			//* for each state do:
//			for (int stateNumber = 1; stateNumber < myGraph.Size; stateNumber++) {
//				bool groupFound = false;
//				//* compare state's output with other goups
//				for (int j = 0; j < groupHeaders.Count; j++) {
//					bool itIsOk = true;
//					foreach (ISymbol symb in inputAlphabet.AllSymbols()) {
//						ISymbol o1 = null, o2 = null;
//
//						//* check in state stateNumber
//						foreach (TRANSITIONTYPE t in myGraph.TransitionsOf(myGraph[stateNumber])) {
//							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
//								o1 = (t as MealyMachine.Mealy_Transition).outLabel;
//								break;
//							}
//						}
//
//						//* check in the header
//						foreach (TRANSITIONTYPE t in myGraph.TransitionsOf(myGraph[groupHeaders[j]])) {
//							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
//								o2 = (t as MealyMachine.Mealy_Transition).outLabel;
//								break;
//							}
//						}
//
//						if (!((o1 == null && o2 == null) || (o1 != null && o1.Equals (o2)))) {
//							itIsOk = false;
//							break;
//						}
//					}
//					if (itIsOk) {
//						partitionTable [stateNumber] = j;
//						groups [j].Add (stateNumber);
//						groupFound = true;
//						break;
//					}
//				}
//				if (!groupFound) {
//					//* it is the header of a new group
//					groupHeaders.Add (stateNumber);
//
//					partitionTable [stateNumber] = groupHeaders.Count - 1;
//
//					groups.Add (new List<int> ());
//					groups [groups.Count - 1].Add (stateNumber);
//				}
//			}
//
//			//* convert the state space to matrix: we will need it!
//			int[][] stateTransitionTable = NewTwoDimArray<int> (myGraph.Size, inputAlphabet.Size);
//
//			//* for each state
//			for (int i = 0; i < myGraph.Size; i++) {
//				//* for each symbol in the alphabet
//				for (int j = 0; j < inputAlphabet.Size; j++) {
//					MealyMachine.Mealy_State target = null;
//					//find the target state for symb[j]
//					//* for each transition
//					for (int k = 0; k < myGraph.TransitionsOf(myGraph[i]).Count; k++) {
//						if ((myGraph.TransitionsOf (myGraph [i]) [k] as MealyMachine.Mealy_Transition).inLabel.Equals (inputAlphabet.AllSymbols () [j])) {
//							target = (myGraph.DestinationOf ((myGraph.TransitionsOf (myGraph [i]) [k])) as MealyMachine.Mealy_State);
//							break;
//						}
//					}
//					int targetIndex = -1;
//					//* find index of target in the machine
//					if (target != null) {
//						for (int l = 0; l < myGraph.Size; l++) {
//							if (target == (myGraph [l] as MealyMachine.Mealy_State)) {
//								targetIndex = l;
//								break;
//							}
//						}
//					}
//
//					//* set the value in table
//					stateTransitionTable [i] [j] = targetIndex;
//				}
//			}
//
//			#endregion
//
//			//* this is last number of partitions in 1-equivalence
//			//int lastNumerOfPartitions = groups.Count;
//			List<int[]> listOfPartitionTables = new List<int[]> ();
//			listOfPartitionTables.Add (CloneArray (partitionTable));
//
//			List<int> toBeSeparated = new List<int> ();
//
//			//* continue till converging the algorithm
//			while (true) {
//				bool somethingChanged = false;
//				//* for each group, check that the outgoing row is the same for all states in the group
//				for (int g = 0; g < groups.Count; g++) {
//					if (groups [g].Count == 1)
//						continue;
//
//					//* index1 in the group
//					for (int i = 0; i < groups[g].Count - 1; i++) {
//						//* index2 in the group
//						int j = i + 1;
//						int index1, index2, index3;
//
//						index1 = groups [g] [i];
//						index2 = groups [g] [j];
//						//* check the groups of destinations for the two row
//						int eq = SameRow (stateTransitionTable, partitionTable, inputAlphabet.Size, index1, index2);
//						if (eq != -1) {
//							somethingChanged = true;
//
//							toBeSeparated.Clear ();
//							toBeSeparated.Add (j);
//
//							//* find those that have equal rwo with index3
//							for (int l = j + 1; l < groups[g].Count; l++) {
//								//if (l == i || l == j)
//								//    continue;
//
//								index3 = groups [g] [l];
//								//* check other elements in the group: they are similar to index1 or not?
//								int eq2 = SameRow (stateTransitionTable, partitionTable, inputAlphabet.Size, index1, index3);
//								if (eq2 == -1)
//									toBeSeparated.Add (l);
//							}
//
//							//* create a new group for state[index1];
//							groups.Add (new List<int> ());
//
//							for (int y = toBeSeparated.Count - 1; y >= 0; y--) {
//								int yy = toBeSeparated [y];
//								int z = groups [g] [yy];
//
//								groups [g].RemoveAt (yy);
//								groups [groups.Count - 1].Add (z);
//								partitionTable [z] = groups.Count - 1;
//							}
//
//							//* store partition table
//							listOfPartitionTables.Add (CloneArray (partitionTable));
//
//							break;
//						}
//					}
//					if (somethingChanged)
//						break;
//				}
//
//				//* this will happen when it converged
//				if (!somethingChanged)
//					break;
//			}
//
//			#endregion

			#region Compute k-equivalence partitions
			#region Initialize

			//* initialize groups [compute 1-equivalence partition]  
			//* for each state do:
			for (int stateNumber = 1; stateNumber < myGraph.Size; stateNumber++) {
				bool groupFound = false;
				//* compare state's output with other goups
				for (int j = 0; j < groupHeaders.Count; j++) {
					bool itIsOk = true;
					foreach (ISymbol symb in inputAlphabet.AllSymbols()) {
						ISymbol o1 = null, o2 = null;

						//* check in state stateNumber
						foreach (TRANSITIONTYPE t in myGraph.TransitionsOf(myGraph[stateNumber])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o1 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;

							}
						}

						//* check in the header
						foreach (TRANSITIONTYPE t in myGraph.TransitionsOf(myGraph[groupHeaders[j]])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o2 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;
							}
						}

						if (!((o1 == null && o2 == null) || (o1 != null && o1.Equals (o2)))) {
							itIsOk = false;
							break;
						}
					}
					if (itIsOk) {
						partitionTable [stateNumber] = j;
						groups [j].Add (stateNumber);
						groupFound = true;
						break;
					}
				}
				if (!groupFound) {
					//* it is the header of a new group
					groupHeaders.Add (stateNumber);

					partitionTable [stateNumber] = groupHeaders.Count - 1;

					groups.Add (new List<int> ());
					groups [groups.Count - 1].Add (stateNumber);
				}
			}

			//* convert the state space to matrix: we will need it!
			//FIXME: this is state transition target table
			int[][] stateTransitionTable = NewTwoDimArray<int> (myGraph.Size, inputAlphabet.Size);

			int[][] stateTransitionOutputTable = NewTwoDimArray<int> (myGraph.Size, inputAlphabet.Size);

			Alphabet outputAlpha = new Alphabet ();

			//* for each state
			for (int i = 0; i < myGraph.Size; i++) {
				//* for each symbol in the alphabet
				for (int j = 0; j < inputAlphabet.Size; j++) {
					MealyMachine.Mealy_State target = null;
					ISymbol ot = null;

					//find the target state for symb[j]
					//FIXME: we can simply use IndexOf!
					//* for each transition
					for (int k = 0; k < myGraph.TransitionsOf(myGraph[i]).Count; k++) {
						if ((myGraph.TransitionsOf (myGraph [i]) [k] as MealyMachine.Mealy_Transition).inLabel.
						    Equals (inputAlphabet.AllSymbols () [j])) {
							target = (myGraph.TransitionsOf (myGraph [i]) [k] as MealyMachine.Mealy_Transition).Destination;
							ot = (myGraph.TransitionsOf (myGraph [i]) [k] as MealyMachine.Mealy_Transition).outLabel;
							break;
						}
					}
					int targetIndex = -1;
					int outputIndex = -1;

					//* find index of target in the machine
					if (target != null) {
						for (int l = 0; l < myGraph.Size; l++) {
							if (target == (myGraph [l] as MealyMachine.Mealy_State)) {
								targetIndex = l;
								if (outputAlpha.Rank (ot) != -1) {
									outputIndex = outputAlpha.Rank (ot);
								} else {
									outputAlpha.AddSymbol (ot);
									outputIndex = outputAlpha.Rank (ot);
								}
								break;
							}
						}
					}

					//* set the value in table
					stateTransitionTable [i] [j] = targetIndex;
					stateTransitionOutputTable [i] [j] = outputIndex;
				}
			}

			#endregion
			List<int[]> listOfPartitionTables = new List<int[]> ();
			listOfPartitionTables.Add (CloneArray (partitionTable));

			List<int> toBeSeparated = new List<int> ();
			int numberOfGroups = groups.Count;

			//* continue till converging the algorithm
			while (true) {
				bool somethingChanged = false;

				int[] tempPartion = CloneArray (partitionTable);

				//* create groups from scratch
				groups.Clear ();
				for (int i=0; i<numberOfGroups; i++)
					groups.Add (new List<int> ());
				for (int i=0; i<partitionTable.Length; i++)
					groups [partitionTable [i]].Add (i);


				for (int currentGroup = 0; currentGroup < groups.Count; currentGroup++) {
					//* this group has only one state
					if (groups [currentGroup].Count == 1)
						continue;

					//* index1 in the group
					for (int i = 1; i < groups[currentGroup].Count; i++) {
						//* index2 in the group

						int state1, state2, state3;

						state1 = groups [currentGroup] [0];
						state2 = groups [currentGroup] [i];

						//* check the groups of destinations for the two row
						int eq = SameRow (stateTransitionOutputTable, stateTransitionTable, partitionTable, inputAlphabet.Size, state1, state2);
						if (eq != -1) {
							somethingChanged = true;
							//* add a new group!
							numberOfGroups++;
							toBeSeparated.Clear ();
							toBeSeparated.Add (i);

							//* find all of those that have equal row with state2
							for (int j = i + 1; j < groups[currentGroup].Count; j++) {
								state3 = groups [currentGroup] [j];

								//* check other elements in the group: they are similar to index1 or not?
								int eq2 = SameRow (stateTransitionOutputTable, stateTransitionTable, partitionTable, inputAlphabet.Size, state2, state3);
								if (eq2 == -1) {
									toBeSeparated.Add (j);
									//[Ali]: I comment this (17 March 2015)
									//groups [currentGroup].RemoveAt (j);
								}
							}

							//* and add all different state into that group
							for (int y = 0; y<toBeSeparated.Count; y++) {
								int indexOfDiffState = toBeSeparated [y];
								int diffState = groups [currentGroup] [indexOfDiffState];
								tempPartion [diffState] = numberOfGroups - 1;
							}
							//* remove 'separateds' from current group
							for (int y = 1; y<toBeSeparated.Count; y++) {
								groups [currentGroup].RemoveAt (y);
							}
						}
					}
				}

				//* this will happen when it converged
				if (!somethingChanged)
					break;
				else {
					//* store partition table
					listOfPartitionTables.Add (CloneArray (tempPartion));
					partitionTable = tempPartion;
				}
			}

			#endregion
			if (groups.Count != myGraph.Size)
				throw new Exception ("The model is not minimal!");


			//* now, from list of partitions,
			//* find the distinguishing string for each pair of states
			for (int i = 0; i < myGraph.Size; i++) {
				for (int j = i + 1; j < myGraph.Size; j++) {
					int startFrom = -1;

					//* find the partition that state i and state j are different
					for (int k = listOfPartitionTables.Count - 2; k >= 0; k--) {
						if (listOfPartitionTables [k] [i] != listOfPartitionTables [k] [j])
							continue;
						startFrom = k;
						break;
					}
					Word w = new Word ();
					int index1 = i, index2 = j;

					//* from that partition, go backward
					for (int k = startFrom; k >= 0; k--) {
						int l = SameRow (stateTransitionTable, listOfPartitionTables [startFrom], inputAlphabet.Size, index1, index2);
						w.AddSymbol (inputAlphabet.AllSymbols () [l]);
						index1 = stateTransitionTable [index1] [l];
						index2 = stateTransitionTable [index2] [l];
					}

					foreach (ISymbol symb in inputAlphabet.AllSymbols()) {
						ISymbol o1 = null, o2 = null;

						//* check in state stateNumber
						foreach (TRANSITIONTYPE t in myGraph.TransitionsOf(myGraph[index1])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o1 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;
							}
						}

						//* check in the header
						foreach (TRANSITIONTYPE t in myGraph.TransitionsOf(myGraph[index2])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o2 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;
							}
						}

						if (!((o1 == null && o2 == null) || (o1 != null && o1.Equals (o2)))) {
							w.AddSymbol (symb);
							break;
						}
					}
					if (computeAll)
						DistinguishingWords4Pairs.Add (w);

					if (!DistinguishingWords.Contains (w))
						DistinguishingWords.Add (w);
				}
			}
			//ListUtil.WriteList(DistinguishingWords, "-");
			//Console.ReadKey();
			//return DistinguishingWords4Pairs;
			return DistinguishingWords;
		}
	}
}
